FDL - Step of Proof: bnot_bnot_elim

Step of Proof: bnot_bnot_elim

Inference at * 1
Iof proof for Lemma bnot bnot elim:

1. p :

(

p) = p

by BoolEval

1:

1: (no hyps)

1:

tt = tt

2:

2: (no hyps)

2:

ff = ff

.

Definitions tt, ff, if b then t else f fi , b, t T, Unit, ,